perm filename EX.ANS[1,JRA] blob sn#028940 filedate 1973-03-14 generic text, type T, neo UTF8
00005	
00010	VAR:x,y,z,u,v,w;
00020	PRE_PRED:P;
00030	PRE_OP:G,E;
00100	P(x,G(x),E);
00200	P(x,E,x);
00300	¬P(x,y,z) ∨ ¬P(y,u,v) ∨ ¬P(x,v,w) ∨ P(z,u,w);
00400	¬P(x,y,z) ∨ ¬P(y,u,v) ∨ ¬P(z,u,w) ∨ P(x,v,w);
00700	THEOREM:∀(x)∃(y)P(y,x,E);
00800	;